Nuprl Definition : alle-le
0,22
postcript
pdf
e
e'
.
P
(
e
) ==
e
:E.
e
e'
P
(
e
)
latex
clarification:
alle-le(
es
;
e'
;
e
.
P
(
e
)) ==
e
:es-E(
es
). es-le(
es
;
e
;
e'
)
P
(
e
)
latex
Definitions
x
:
A
.
B
(
x
)
,
E
,
P
Q
,
e
e'
FDL editor aliases
alle-le
origin
e
e'.P(e) == e:E. e e' 
P(e)
e:es-E(es). es-le(es;e;e') P(e) ee'.P(e) == e:E. e e' P(e)
e:es-E(es). es-le(es;e;e') P(e) x:A. B(x) Q e'